//
// Created by xux on 2024/9/11.
//
#pragma once
#ifndef CL4AF_SOLVER_H
#define CL4AF_SOLVER_H


#define NO_CONFLICT (-1)
#define CONFLICT 0
#define CONFLICT_ON_BASE (-2)
#define CLAUSE_INFER (-3)

#define SUCCESS_DECISION 0
#define DECISION {}

#define NO_BLANK_ARG (-1)

#define LIT_SAT 1
#define LIT_UNSAT (-1)
#define LIT_UNASSIGNED 0

#include <cassert>
#include <string>
#include <vector>
#include <unordered_map>
#include <list>
#include <fstream>
#include <iostream>
#include <memory>
#include <queue>
#include <unordered_set>
#include <numeric>

#include "Heap.h"
#include "Clause.h"
#include "log.h"
#include "Bitset.h"

class Solver {
private:
    const int           LBD_QUEUE_DEFAULT_CAPACITY = 50;
    int                 rephase_threshold = 0,
                        rephase_limit = 1024,
                        rephases = 0,
                        *lbd_queue,
                        lbd_queue_size = 0,
                        lbd_queue_pos = 0,
                        propagated,             // 已传播争议的位置
                        arg_number,             // 争议个数,
                        current_level,          // 记录当前层次
                        restart_counter = 0,        // 重启计数器
                        restart_threshold,
                        luby_step,
                        reduce_counter = 0,
                        reduce_limit = 2000,
                        reduce_increment = 300,
                        global_counter = 0,
                        conflicts = 0;
    std::vector<int>    saved,
                        local_best,
                        args,                   // 争议集
                        depth,                  // 争议所在层次
                        label;                  // 争议的标签
    std::vector<double> activity;
    double              activity_inc = 1,
                        restart_inc = 1.5,
                        fast_lbd_sum = 0,
                        slow_lbd_sum = 0;
    std::list<int>      conflict;               // 冲突争议集
    std::vector<std::vector<int>>           reasons,                 // 争议被赋值的原因
                                            attack,                // 攻击关系
                                            attack_by;             // 被攻击争议
    std::shared_ptr<Heap>                   arguments_to_label;     // 标签为blank的争议
    std::vector<std::string>                id2argument;    // 将int转为string类型
    std::unordered_map<std::string, int>    argument2id;    // 将string转为int类型
    std::vector<std::tuple<int,int,int>>    trail;          // 记录用于回溯的信息{arg, label, depth, reason}
    std::string file;
    std::vector<Clause>clause_DB;
    std::vector<std::vector<int>> watches;


    int decide();
    std::tuple<Clause, int, int, int> analyze();
    void backtrack(int backtrack_level);
    int propagate();
    int IN_propagate(int arg);
    int OUT_propagate(int arg);
    int clause_propagate(int arg);
    void reduce();
    void restart();

    static double luby(double y, int x);
    void rephase();
    void update_activity(int arg, double coeff);
    bool is_legal_must_out(int arg);
    double hval(int arg);
    void set_infer(int arg, int lab, std::vector<int>&& reason);
    void set_label(int arg, int lab);
    int get_label(int arg);
    void alloc_memory(size_t size);
    void init_label();
    void add_clause(Clause &&clause);
    static char label2char(int lab);
    int lit_is_sat(int lit);
    void print_ans();
    void read_TGF(const std::string& filename);
    void read_AF(const std::string& filename);
public:
    void read_file(const std::string& filename);
    void solve();
};


#endif //CL4AF_SOLVER_H
